$\forall$$T$:Type, $l$:($T$ List), $P$:($T$$\rightarrow\mathbb{B}$), $x$,$y$:$T$.
\\[0ex]l\_before($x$; $y$; filter($P$; $l$); $T$) $\Leftarrow\!\Rightarrow$ (($\uparrow$($P$($x$))) $\wedge$ ($\uparrow$($P$($y$))) $\wedge$ l\_before($x$; $y$; $l$; $T$))